\begin{tabbing}
combine{-}ecl{-}tuples2($A$;$B$;$f$;$g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let ${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$ = $A$ in \+
\\[0ex]let ${\it Tb}$,${\it ksb}$,${\it ib}$,${\it gb}$,${\it hb}$,${\it ab}$,${\it eb}$ = $B$ in 
\\[0ex]$\langle$(${\it Ta}$$\times$${\it Tb}$$\times$($\mathbb{B}$+Unit))
\\[0ex]$,\,$(${\it ksa}$ @ ${\it ksb}$)
\\[0ex]$,\,$$\langle$${\it ia}$$,\,$${\it ib}$$,\,$inr($\cdot$)$\rangle$
\\[0ex]$,\,$($\lambda$${\it k'}$,$s$,$v$,$x$. \=let ${\it sa}$ = \=if deq{-}member(KindDeq;${\it k'}$;${\it ksa}$)$\rightarrow$ ${\it ga}$(${\it k'}$,$s$,$v$,1of($x$))\+\+
\\[0ex]else 1of($x$) fi in 
\-\\[0ex]let ${\it sb}$ = \=if deq{-}member(KindDeq;${\it k'}$;${\it ksb}$)$\rightarrow$ ${\it gb}$(${\it k'}$,$s$,$v$,1of(2of($x$)))\+
\\[0ex]else 1of(2of($x$)) fi in 
\-\\[0ex]$\langle$${\it sa}$$,\,$${\it sb}$$,\,$combine{-}halt{-}info(${\it ea}$;${\it eb}$;$\lambda$$m$.${\it ha}$($m$,${\it sa}$);$\lambda$$m$.${\it hb}$($m$,${\it sb}$);2of(2of($x$)))$\rangle$)
\-\\[0ex]$,\,$($\lambda$$n$,$x$. $f$(2of(2of($x$)),$\lambda$$m$.${\it ha}$($m$,1of($x$)),$\lambda$$m$.${\it hb}$($m$,1of(2of($x$))),$n$))
\\[0ex]$,\,$($\lambda$$n$,${\it k'}$,$s$,$v$,$x$. \=$g$\+
\\[0ex](${\it ha}$(0,1of($x$))
\\[0ex],${\it hb}$(0,1of(2of($x$)))
\\[0ex],reduce($\lambda$$m$,$b$. ${\it ha}$($m$,1of($x$)) $\vee_{2}$ $b$;false$_{2}$;${\it ea}$)
\\[0ex],reduce($\lambda$$m$,$b$. ${\it hb}$($m$,1of(2of($x$))) $\vee_{2}$ $b$;false$_{2}$;${\it eb}$)
\\[0ex],if deq{-}member(KindDeq;${\it k'}$;${\it ksa}$)$\rightarrow$ ${\it aa}$($n$,${\it k'}$,$s$,$v$,1of($x$)) else false$_{2}$ fi
\\[0ex],\=if deq{-}member(KindDeq;${\it k'}$;${\it ksb}$)$\rightarrow$ ${\it ab}$($n$,${\it k'}$,$s$,$v$,1of(2of($x$)))\+
\\[0ex]else false$_{2}$ fi))
\-\-\\[0ex]$,\,$merge(${\it ea}$;${\it eb}$)$\rangle$
\-
\end{tabbing}